secret{-}table($T$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$K$:$\mathbb{N}\times\mathbb{N}\times$(\{0..$K$$^{-}$\}$\rightarrow$Atom1$\times$($\mathbb{N}$+Atom1)$\times$data($T$))